$\forall$${\it es}$:ES, $i$, $x$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $k$:Knd, $T$:Type, $f$:(State(${\it ds}$)$\rightarrow$$T$$\rightarrow$DeclaredType(${\it ds}$;$x$)).
\\[0ex]@$i$ events of kind $k$ change $x$ to $f$ State(${\it ds}$) (val:$T$) $\in$ Prop